L22 - Model Checking

Testing Vs Model Checking
- Testing
	- informal specification
	- cannot exhausively check the system
	- widely used technique in practice
- Model Checking
	- work on model of program
	- target current sytem
	- successful in hardware systems + comm. protocol.


Verification Process
1. Modeling
	- convert design into formalism accepted by model checking tool
2. Specification
	- state properties to satisfy
3. Verification
	- completely automatic
	- produce result w/ error trace

Advantages
- fully autmoated
- produce error example

Properties Categories
- safety --> "nothing bad can happen"
	- !> 2 processes in critical section at same time
- liveness --> "something good will happen"
	- if process want acess to critical section, it will
- fairness --> every request is eventually granted
	- 
